ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A,B:ecl-trans-tuple{i:l}(ds; da),
f:(()()), g:().
combine-ecl-tuples(A; B; f; g)  ecl-trans-tuple{i:l}(ds; da) 

latex

Definitions

t  T, x:A. B(x), decl-state(ds), ma-valtype(da; k), ff, Knd, (x  l), b, prop{i:l}, A, b, , A  B, P  Q, False, , x. t(x), t.2, t.1, band(p; q), P  Q, P  Q, Unit, if b then t else f fi , append(as; bs), strong-subtype(A; B), EqDecider(T), fpf(A; a.B(a)), fpf-cap(f; eq; x; z), , merge(as; bs), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), combine-ecl-tuples(A; B; f; g), ecl-trans-tuple{i:l}(ds; da), Id, Kind-deq, deq-member(eq; x; L)

Lemmas

ecl-trans-tuple wf, fpf wf, Id wf, merge wf, nat plus wf, nat wf, nat properties, strong-subtype-deq-subtype, strong-subtype-set3, strong-subtype-self, subtype rel self, l member subtype, append wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, band wf, pi1 wf, pi2 wf, le wf, bool wf, bnot wf, not wf, assert wf, l member wf, Knd wf, Kind-deq wf, bfalse wf, ma-valtype wf, decl-state wf